$\forall$$A$, $B$:Type, $g$:($A$$\rightarrow$($B$ + Top)), $X$:MaInterface($A$), ${\it es}$:ES, $e$:E.
\\[0ex]ma{-}in{-}interface(${\it es}$;ma{-}interface{-}compose($g$;$X$);$e$) $\sim$ ma{-}in{-}interface(${\it es}$;$X$;$e$)